(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun f (Real) Real)
(assert (= (+ x x) 2))
(assert (= (* y y) 2 (* z z)))
(assert (distinct (f x) (f y)))
(assert (= (f x) (f z)))
(assert (distinct (f (/ x y)) (f (+ x z))))
(check-sat)
